Exhaustively checking one or more properties in each and every possible state (e.g. of size 1000 bits) and each and every possible input combination to each state by simulation, (e.g. using test vectors) is prohibitively expensive. For this reason, digital circuits (portions thereof or in their entirety) are often analyzed by formal verification, to determine the validity of one or more properties that describe correct and incorrect behaviors in the circuit.
Formal verification of properties can use any of a variety of methods to prove that it is impossible to violate a given property, starting from an initial state or set of initial states of the digital circuit. Tools for formal verification of properties that are available in the prior art (either commercially or from public sources such as universities and laboratories) may be based on any of a number of techniques, such as (1) symbolic model checking, (2) symbolic simulation, (3) explicit state enumeration, and (4) satisfiability (SAT). For background on each of the just-described techniques, see, for example, the following references, each of which is incorporated by reference herein in its entirety:                (1) an article by J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang, entitled “Symbolic model checking: 1020 states and beyond”, published in Information and Computation, Vol. 98, no. 2, June 1992; another article entitled “Coverage Estimation for Symbolic Model Checking” by Yatin Hoskote, Timothy Kam, Pei-Hsin Ho, and Xudong Zhao, published in Proceedings of DAC 1999 (Best Paper Award), pp. 300-305, and a PhD thesis by K. L. McMillan entitled “Symbolic model checking—an approach to the state explosion problem”, Carnegie Mellon University, 1992;        
(2) article entitled “Automatic Verification of Pipelined Microprocessor Control,” by Jerry R. Burch and David L. Dill, published in the proceedings of International Conference on Computer-Aided Verification, LNCS 818, Springer-Verlag, June 1994;
(3) article by E. M. Clarke, E. A. Emerson and A. P. Sistla entitled “Automatic verification of finite-state concurrent systems using temporal logic specifications” published in ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986; and article entitled “Protocol Verification as a Hardware Design Aid” by David Dill, Andreas Drexler, Alan Hu and C. Han Yang published in Proceedings of the International Conference on Computer Design, October 1992.
(4) article entitled “Bounded Model Checking Using Satisfiability Solving” by Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu, published in Formal Methods in System Design, volume 19 issue 1, July 2001, by Kluwer Academic Publishers.
In addition, see U.S. Pat. No. 5,465,216 granted to Rotem, et al. on Nov. 7, 1995, and entitled “Automatic Design Verification” (that is incorporated by reference herein in its entirety) for an additional example of formal verification tool. See also U.S. Pat. No. 6,192,505 granted to Beer, et al. on Feb. 20, 2001, and entitled “Method and system for reducing state space variables prior to symbolic model checking” that is incorporated by reference herein in its entirety.
Formal verification tools available in the prior art for property checking include, for example, Symbolic Model Verification (SMV) software package available from Carnegie-Mellon University, the coordinated specification analysis (COSPAN) software package available from Bell Laboratories (e.g. at ftp.research.att.com), and the VIS package available from University of California, Berkeley.
For additional information on formal verification tools, see C. Kern and M. R. Greenstreet, “Formal Verification in Hardware Design: A Survey,” in ACM Trans. on Design Automation of Electronic Systems, vol. 4, pp. 123-193, April 1999 that is incorporated by reference herein in its entirety.
Such formal verification tools normally operate on a description of the digital circuit (also called “circuit-under-verification”), which is generated from a hardware description language (HDL) such as Verilog (see “The Verilog Hardware Description Language,” Third Edition, Don E. Thomas and Philip R. Moorby, Kluwer Academic Publishers, 1996) or VHDL (see “A Guide to VHDL”, Stanley Mazor and Patricia Langstraat, Kluwer Academic Publishers, 1992).
Therefore, during prior art testing of a digital circuit, properties or assertions about the correct and incorrect behaviors of the circuit may be checked using a formal verification tool. The properties are normally described using a HDL language such as Verilog or using a property specification language such as Sugar (e.g. available from IBM Research Labs, Haifa, Israel). To validate the correctness of a digital circuit, the formal verification tool must check many properties. The properties may be checked individually sequentially or combined simultaneously. The formal verification tool may start from a single initial state or from a set of initial states for each property.
One method for formal verification of properties is based on so-called bounded model checking (BMC). Such a method may use a Boolean formula that is TRUE if and only if the underlying state transition system can realize a sequence of state transitions that reaches certain states of interest within a fixed number of transitions. If such a sequence cannot be found at a given length, k, the search is continued for larger k. The procedure is symbolic, i.e., symbolic Boolean variables are utilized; thus, when a check is done for a specific sequence of length k, all sequences of length k from an initial plate are examined. A Boolean formula that is formed for each sequence is used by the tool, and if a satisfying assignment is found, that assignment is a “witness” (also called “counter example”) for the sequence of interest.
Such a formal verification tool has three possible results for each Boolean formula: the formula is proven true; a counter-example is produced; or the tool cannot determine the truth of the Boolean formula because memory or compute resource limits prevent completion of the checking. The last-described result (i.e. “cannot determine”) is often the case when such a tool is applied to a real-world digital circuit (such as a microprocessor) that has a large number of transistors (in the order of 1-5 million), because of the well known “state explosion problem”
As described in “Architecture Validation for Processors”, by Richard C. Ho, C. Han Yang, Mark A. Horowitz and David L. Dill, Proceedings 22.nd Annual International Symposium on Computer Architecture, pp. 404-413, June 1995, “modern high-performance microprocessors are extremely complex machines which require substantial validation effort to ensure functional correctness prior to tapeout” (see page 404). As further described in “Validation Coverage Analysis for Complex Digital Designs” by Richard C. Ho and Mark A. Horowitz, Proceedings 1996 IEEE/ACM International Conference on Computer-Aided Design, pp. 146-151, November 1996, “the functional validation of state-of-the-art digital design is usually performed by simulation of a register-transfer-level model” (see page 146).
A number of metrics for verification tools are described in the prior art, for example, see the following articles:
(1) Hoskote, Y. V., et al., “Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors”, International Conference on Computer Design: VLSI in Computers & Processors, Oct. 2-4, 1995, pp. 532-537;
(2) Moundanos, D., “Abstraction Techniques for Validation Coverage Analysis and Test Generation”, IEEE Transactions on Computers, vol. 47, January 1998, pp. 2-14;
(3) Devadas, S., et al., “An Observability-Based Code Coverage Metric for Functional Simulation”, IEEE/ACM International Conference on Computer-Aided Design, Nov. 10-14, 1996, pp. 418-425; and
(4) Geist, D., et al., “Coverage-Directed Test Generation Using Symbolic Techniques”, Formal Methods in Computer-Aided Design, First International Conference, FMCAD 96, Palo Alto, Calif., Nov. 6-8, 1996, pp. 142-159.
Each of the above-referenced articles (1)-(4) is incorporated by reference herein in its entirety.
See U.S. Pat. No. 6,102,959 granted to Hardin, et al. on Aug. 15, 2000 and entitled “Verification tool computation reduction” that is incorporated by reference herein in its entirety.
U.S. Pat. No. 6,311,293 granted to Kurshan, et al. on Oct. 30, 2001 and entitled “Detecting of model errors through simplification of model via state reachability analysis” that is incorporated by reference herein in its entirety.
Also incorporated by reference herein in their entirety are the following: U.S. Pat. No. 6,356,858 granted to Malka, et al. on Mar. 12, 2002 and entitled “Coverage measurement tool for user defined coverage models”; U.S. Pat. No. 5,724,504 granted to Aharon, et al. on Mar. 3, 1998 and entitled “Method for measuring architectural test coverage for design verification and building conformal test”.
Also incorporated by reference herein in their entirety are the following references:
“Algorithms for the Satisfiability (SAT) problem: A Survey” by Jun Gu, Paul W. Purdom, John Franco, and Benjamin W. Wah, DIMACS Series on Discrete Mathematics and Theoretical Computer Science 35:19-151, American Mathematical Society, 1997;
“A machine program for therorem-proving” by Martin Davis, George Longemann, and Donald Loveland in Communications of the ACM, 5(7):394-497, July 1962; and
“Chaff: Engineering an Efficient SAT Solver” by M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, in 38th Design Automation Conference (DAC '01), June 2001, pp. 530-535.